$\forall$$T$:Type, $L$:$T$ List, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$$T$). ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $f$($i$) $=$ $L$[$i$]) $\Rightarrow$ $L$ $=$ map($f$;upto($\parallel$$L$$\parallel$))